a, b:. Dec(a | b) 

latex

Definitions	x:A. B(x), t  T, Dec(P), P  Q, A, b | a, False, P  Q, Prop, a  b, P  Q, P & Q, P  Q,
Lemmas	nequal wf, divides iff rem zero, iff preserves decidability, zero divs only zero, divides wf, not wf, divides reflexivity, decidable int equal